/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ β5G␈↓
:␈↓αODEL'S LEMMA AND APPLICATIONS IN FIRST ORDER LISP

␈↓ α∧␈↓␈↓ αTThe␈α⊗object␈α⊗of␈α⊗this␈α⊗note␈α⊗is␈α⊗to␈α⊗give␈α⊗a␈α⊗compact␈α⊗treatment␈α⊗of␈α⊗G␈↓
:␈↓odel's␈α⊗Lemma␈α⊗in␈α⊗an
␈↓ α∧␈↓axiomatization␈α
of␈α
Lisp␈α
in␈α∞a␈α
first␈α
order␈α
logic␈α
fortified␈α∞by␈α
first␈α
order␈α
lambda␈α
notation.␈α∞ The␈α
Lisp
␈↓ α∧␈↓G␈↓
:␈↓odel␈α
numbering␈α
trivial␈αby␈α
letting␈α
expressions␈α
be␈αtheir␈α
own␈α
G␈↓
:␈↓odel␈αnumbers,␈α
and␈α
the␈α
first␈αorder
␈↓ α∧␈↓lambdas␈α~enable␈α~one␈α~to␈α~avoid␈α≠the␈α~circumlocutions␈α~of␈α~the␈α~conventional␈α≠treatment.␈α~ The
␈↓ α∧␈↓circumlocutions␈α
arise␈α
from␈α
the␈α
fact␈α
that␈α
G␈↓
:␈↓odel's␈α
lemma␈α
is␈α
really␈α
about␈α
the␈α
application␈α
of␈α
first␈α
order
␈↓ α∧␈↓predicate␈α
expressions␈α
to␈α
themselves,␈α
but␈α
a␈α
logic␈α
not␈α
admitting␈α
complex␈α
predicate␈α
expressions␈αhas␈α
to
␈↓ α∧␈↓get␈αaround␈αthis␈α
fact␈αby␈αusing␈α
wffs␈αwith␈αone␈α
free␈αvariable␈αand␈α
taking␈αthis␈αvariable␈α
to␈αbe␈α␈↓↓x␈↓␈αor␈α
some
␈↓ α∧␈↓other standard name.

␈↓ α∧␈↓␈↓ αTAdding␈αfirst␈αorder␈αlambdas␈αto␈αfirst␈αorder␈αlogic␈αdoes␈αnot␈αchange␈αits␈αbasic␈αcharacter,␈αbecause
␈↓ α∧␈↓any␈α
wff␈α
containing␈α∞them␈α
can␈α
be␈α
transformed␈α∞to␈α
an␈α
equivalent␈α
wff␈α∞without␈α
them␈α
by␈α∞making␈α
the
␈↓ α∧␈↓indicated␈α
lambda␈α
conversions.␈α
 As␈α
will␈α∞be␈α
seen,␈α
however,␈α
it␈α
makes␈α
the␈α∞metamathematics␈α
simpler,
␈↓ α∧␈↓and it has other advantages for mathematical theory of computation.

␈↓ α∧␈↓␈↓ αTG␈↓
:␈↓odel's␈α∂lemma␈α∞is␈α∂a␈α∞key␈α∂technical␈α∞result␈α∂making␈α∞possible␈α∂proofs␈α∞of␈α∂G␈↓
:␈↓odel's␈α∞incompleteness
␈↓ α∧␈↓theorems␈α∞in␈α∞various␈α∞forms,␈α∞Tarski's␈α∞theorem␈α∞on␈α∞the␈α∞undefinability␈α∞of␈α∞truth,␈α∞and␈α∞other␈α∞negative
␈↓ α∧␈↓results␈α
of␈α
recursive␈α
function␈α
theory␈α
and␈α
formalized␈α
arithmetic.␈α
 G␈↓
:␈↓odel␈α
imbedded␈α
a␈α
special␈α
case␈αin␈α
a
␈↓ α∧␈↓longer␈αproof,␈αand␈αother␈αauthors␈αhave␈α
isolated␈αit.␈α For␈αan␈αelegant␈αconventional␈αtreatment␈α
we␈αrefer
␈↓ α∧␈↓to (Boolos and Jeffrey 1974).

␈↓ α∧␈↓␈↓ αTLet ␈↓↓p␈↓ be a one argument predicate expression in Lisp.  We define

␈↓ α∧␈↓1)␈↓ αt ␈↓↓diag p = < p <" p>>␈↓,

␈↓ α∧␈↓which becomes

␈↓ α∧␈↓2)␈↓ αt ␈↓↓(DEF (DIAG P) (L P (L (" ") P))))␈↓

␈↓ α∧␈↓in compact S-expression Lisp.

␈↓ α∧␈↓␈↓ αTLet ␈↓↓b␈↓ be a one place predicate expression, and consider the sentence

␈↓ α∧␈↓3)␈↓ αt ␈↓↓g = ((λ (P) (b (DIAG P))) (" (λ (P) (b (DIAG P)))))␈↓.

␈↓ α∧␈↓Performing␈αthe␈αlambda␈αconversion␈αindicated␈αin␈α(3)␈αand␈αcarrying␈αout␈αthe␈αindicated␈αevaluations␈αof
␈↓ α∧␈↓DIAG applied to quoted arguments gives

␈↓ α∧␈↓4)␈↓ αt  ␈↓↓g␈↓ ∧4= ((λ (P) (b (DIAG P))) (" (λ (P) (b (DIAG P)))))␈↓.

␈↓ α∧␈↓␈↓ ∧4= (b (DIAG (" (λ (P) (b (DIAG P))))))

␈↓ α∧␈↓␈↓ ∧4= (b (L (" (λ (P) (b (DIAG P)))) (L (" ") (" (λ (P) (b (DIAG P)))) )))

␈↓ α∧␈↓␈↓ ∧4= (b (L (" (λ (P) (b (DIAG P)))) (" (" (λ (P) (b (DIAG P))))) ))

␈↓ α∧␈↓␈↓ ∧4= (b (" ((λ (P) (b (DIAG P))) (" (λ (P) (b (DIAG P))))) ))

␈↓ α∧␈↓␈↓ ∧4= (b (" g))
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓␈↓ αTG␈↓
:␈↓odel's Lemma then takes the form

␈↓ α∧␈↓␈↓↓Theorem␈α-␈αIf␈α
b␈αis␈αa␈αpredicate␈α
expression␈αof␈αone␈α
argument␈αin␈αour␈αfirst␈α
order␈αlanguage␈αof␈αLisp,␈α
then
␈↓ α∧␈↓↓there is a wff g satisfying

␈↓ α∧␈↓↓5)␈↓ αt ␈↓πr␈↓↓ g ≡ b <" g>

␈↓ α∧␈↓↓or in S-expression form

␈↓ α∧␈↓↓6)␈↓ αt ␈↓(THEOREM (≡ g (b (LIST (" ") g)))).

␈↓ α∧␈↓␈↓ αTThe␈αproof␈αis␈αjust␈αthe␈αabove␈αcalculation.␈α The␈αonly␈αrules␈αused␈αare␈αlambda␈αconversion,␈α
which
␈↓ α∧␈↓is␈α∂part␈α∂of␈α∂the␈α∂logic␈α∂with␈α∂first␈α⊂order␈α∂lambdas,␈α∂and␈α∂the␈α∂computation␈α∂of␈α∂the␈α∂Lisp␈α⊂function␈α∂LIST
␈↓ α∧␈↓applied to constant arguments.

␈↓ α∧␈↓Remark:␈α
In␈α
the␈α
above␈α
form,␈α
G␈↓
:␈↓odel's␈α
lemma␈α
is␈α
just␈α
an␈α
imitation␈α
of␈α
a␈α
fixed␈α
point␈α
theorem␈α
of␈αthe
␈↓ α∧␈↓lambda␈α
calculus,␈α∞i.e.␈α
that␈α∞[λ␈α
x␈α∞f(x(x))][λ␈α
x␈α∞f(x(x))]␈α
converts␈α∞to␈α
f([λ␈α∞x␈α
f(x(x))][λ␈α∞x␈α
f(x(x))])␈α∞and␈α
is
␈↓ α∧␈↓therefore a fixed point of f.  It is proved by just carrying out the indicated lambda conversion.

␈↓ α∧␈↓Notational␈αconfession:␈αA␈αdesire␈αfor␈αcompactness␈α
has␈αled␈αto␈αcompressing␈αLisp␈αnotation␈αaccording␈α
to
␈↓ α∧␈↓the following table:

␈↓ α∧␈↓␈↓ αT" for QUOTE

␈↓ α∧␈↓␈↓ αTλ for LAMBDA

␈↓ α∧␈↓␈↓ αTL for LIST.

␈↓ α∧␈↓␈↓ αTFurther␈α
confession:␈α
The␈αafore-used␈α
S-expression␈α
theory␈α
of␈αLisp␈α
hasn't␈α
been␈α
written␈αdown.
␈↓ α∧␈↓It␈αis␈αalong␈αthe␈αlines␈αof␈α(Cartwright␈αand␈αMcCarthy␈α1979)␈αbut␈αin␈αS-expressions␈αand␈αsimpler.␈α Since
␈↓ α∧␈↓only␈αa␈αversion␈αanalogous␈αto␈α
Abraham␈αRobinson's␈αQ␈αis␈αrequired,␈α
we␈αdon't␈αneed␈αinduction␈αbut␈α
only
␈↓ α∧␈↓the algebraic properties of the basic functions and the recursive formula

␈↓ α∧␈↓␈↓ αT7)␈↓ αt ␈↓↓x ≤ y ≡ atom x ∨ [¬atom y ∧ [x = y ∨ x ≤ ␈↓αa␈↓↓ y ∨ x ≤ ␈↓αd␈↓↓ y]]␈↓.

␈↓ α∧␈↓␈↓ αTMaybe G␈↓
:␈↓odel's lemma doesn't even require ≤.

␈↓ α∧␈↓␈↓ αTThe applications promised in the title are yet to come.

␈↓ α∧␈↓␈↓ αTReferences:

␈↓ α∧␈↓␈↓ αT␈↓αBoolos,␈αGeorge␈αand␈αRichard␈αJeffrey␈α
(1974)␈↓:␈α␈↓↓Computability␈αand␈αLogic␈↓,␈αCambridge␈α
University
␈↓ α∧␈↓Press.

␈↓ α∧␈↓John McCarthy
␈↓ α∧␈↓Artificial Intelligence Laboratory
␈↓ α∧␈↓Computer Science Department
␈↓ α∧␈↓Stanford University
␈↓ α∧␈↓Stanford, California 94305
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓ARPANET: MCCARTHY@SU-AI

␈↓ α∧␈↓␈↓ αT␈↓εThis␈α∂version␈α⊂of␈α∂G␈↓
:␈↓εODEL[W79,JMC]␈α∂translated␈α⊂for␈α∂printing␈α⊂(by␈α∂PUB)␈α∂at␈α⊂23:59␈α∂on␈α⊂January␈α∂14,
␈↓ α∧␈↓ε1979.␈↓